Nuprl Lemma : member-insert
11,40
postcript
pdf
T
:Type,
eq
:EqDecider(
T
),
a
:
T
,
L
:(
T
List),
b
:
T
. (
b
insert(
eq
;
a
;
L
))
((
b
=
a
)
(
b
L
))
latex
Definitions
EqDecider(
T
)
,
P
Q
,
P
Q
,
(
x
l
)
,
t
T
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
deq
wf
,
insert
property
origin
T:Type, eq:EqDecider(T), a:T, L:(T List), b:T. (b 
insert(eq; a; L)) 
((b = a) 
(b L)) T:Type, eq:EqDecider(T), a:T, L:(T List), b:T. (b insert(eq; a; L)) ((b = a) (b L)) Q Q l) T
Q Qx:A. B(x)